Issue830.agda:8,3-6
Set₁ is not less or equal than Set
when checking that the type Set ⟶ ⟨Set⟩ of the constructor [_] fits
in the sort Set of the datatype.
